COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	  The FOL system has the ability to 
C00016 ENDMK
C⊗;
  The FOL system has the ability to 
enter these general facts into its data base.  Weyhrauch is interested
in the problem of how to incorporate these into deductions and how to 
reason about these facts rather than with them.   

One long term goal is to make computers
carry out the reasoning required to solve problems.  To do this,
we must study what information is required, how it can
be represented in the memory of a computer, and what kinds of reasoning are involved
in solving the problem.  Studying the reasoning involved in problem solving
has two parts: the %2epistemological part%1 and the %2heuristic part%1.  The
%2epistemological%1 part concerns what the desired reasoning is, and the 
%2heuristic%1 part concerns how to make the computer %2find%1 it.
Because the whole artificial intelligence problem has proved very difficult,
it is often worthwhile to concentrate on a part at a time, and our work
is primarily concerned with the %2epistemological part%1. 

Circumscription will be added to FOL.

Artificial Intelligence has proved to be a very difficult branch of science.
In its first fifteen years, the limits of what can be done in a wide
variety of intellectual problems by more or less straightforward
programming were explored.  These problems included game playing
(because comparison with human performance is easy there),
theorem proving (mostly using variants of Robinson's resolution method)
question answering (often on the basis of a theorem
proving program), and many programs embodying an analysis of how humans
search spaces of possible solutions.  A somewhat less popular line
of research involved studying particular intellectual mechanisms such
as learning and trying them out in a variety of problems.  While the
performance of these systems approached and even exceeded human performance
in a few areas, each of them was limited to a narrow domain of application,
and it became clear that the human ability to accept a problem in
a general context of human goals and to isolate the relevant facts and
formulate the search problem in terms of these facts was not being
approached.

Some ideas for general intelligent systems were also explored, but so far
they have not been very powerful problem solvers.  Many problems require
extensive restructuring to fit into the "general" systems, and it became
clear that the restructuring itself was part of the problem the
intelligent system should be able to solve.  The best of this work has
been useful, and there is more to be discovered along these lines.
However, we are exploring a different approach.

Lately the AI field has concentrated much of its attention on what is
called the representation problem - the problem of what information an
intelligent program needs and how it is to be represented in the memory of
a computer.  One of the major approaches is based on the idea that the
%2best%1 way to represent information is in the form of a program that
simulates the behavior of systems being studied or finds objects having
desired properties.

We think that representation of information by programs will have further
successes, but it isn't the whole story.  First, information doesn't
usually become available packaged into programs, and second, much
human information does not %2feel%1 like a program and isn't transmitted
from one person to another as a program.  Therefore, while much information
is most effectively %2used%1 as programs, we have to manipulate it
as facts, and we have to automate the process of going from %2relevant facts%1
to %2useful program%1.  Indeed, this is our conception of automatic
programming.

Many of these considerations were first put forth in [McCarthy 1959] which
first proposed a reasoning program then called the %2Advice Taker%1.  The
Advice Taker was based on the principle "%3In order for a program to be
capable of learning something it must first be capable of being told
it%1," i.e., it must be capable of representing the relevant facts.  In
some sense, we are still pursuing the goals set forth in that paper but
with much more powerful tools than were then available.

The most straightforward applications of proof checking arise in mathematics,
because the logical systems we are using were developed for mathematics.
Indeed, mathematicians have proved informally that proofs in set
theory exist for all classical mathematical theorems.  However, our experience with
the formalization of approximately five such proofs
has shown many ways of reducing their length 
by formalizing heretofore informal modes of reasoning.  These
new modes of reasoning will also be needed in other domains and for a future 
transition
to automatically generated proofs.

The most difficult area is making the computer check common sense reasoning.
The difficulties have several aspects, and we have made some progress in
dealing with each of them.

While the main scientific importance of formal reasoning comes from the part
it plays in the study of general intelligence, it does have some short range 
applications.  In particular Todd Wagner has used
FOL in the area of verifying the correctness of hardware and we intend to use
FOL as the basis for development of a system for reasoning about computer
programs.  See the accomplishments and goals sections below.

.SS The FOL Proof-Checker

Our main work is based on a proof checker for first order logic and 
axiomatizations of different theories within this framework.

  This has a theoretical side called %2mathematical
theory of computation%1 which studies the mathematical properties of 
programs and a practical side - making systems that check the proofs 
of program correctness.  We use FOL to facilitate our research in
theory of computation.

Although theorem proving has a longer history in artificial intelligence
than proof checking, it is important to realize that for large classes of
problems progress can only be made by a proof checking system.  We have
now developed the FOL proof-checker to the state were we can envision how
to represent most of the kinds of reasoning for which it was designed.
[Weyhrauch 1978c] is a collection of FOL proofs.  As we expected they are
longer than human informal proofs, but they are examples of the first
machine-checked complete proofs of substantial results in mathematics,
program correctness, and the theory of knowledge.  Most of the theorems
reported in the memo cannot be automatically proved using existing
provers.  Making these theorems accessible to automatic demonstration by
discovering how to make the arguments shorter is one of the goals of the
FOL project.  Comparing these formal proofs with
those of mathematicians, has given us insights into
how to make improvements to this proof-checking system.  Moreover, the
proof-checking approach includes the automatic theorem proving approach,
because any automatic theorem proving routines that are available can be
included in the proof checker so as to allow anything they can prove to be
done in a single step of the human produced proof.  Several such automatic
provers are already included in FOL.

The semantic attachment feature is being used to connect the logic of FOL to 
situations
in the physical world.  For example, functions and predicates in a logical
system dealing with physical objects and their two dimensional images could
be %2attached%1 to programs that actually use the TV camera.  This will
enable us to study the combination of reasoning and observation that is used
is used in drawing conclusions about physical world scenes.

In turn this will help in formalizing common sense properties of the physical
world which will help in proving the correctness of programs that interact 
with this world.
  The method will be incorporated in FOL in such a way that
general facts about these data bases can be derived and used, e.g. a program
can establish that certain person is not at the M.I.T. AI Lab by using
the general proposition that all such people are in their phone directory
file and using the description of that file to access it and determine
that the person is not in it.  The work differs from most other data
base work in that it works with data bases that other people have designed
without having such applications in mind.